es:ES{i}, ff:FIFO{i:l}(es). F2F+-decls{i:l}(es; ff)  Type{i'} 

latex

Definitions	let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g), [e: i p j], P & Q, ff.C, A c B, , F2F+-decls, t  T, FIFO, x:A. B(x)
Lemmas	top wf, not wf, decidable wf, Id wf, event system wf, fifo wf, es-loc wf, es-state wf, es-E wf, fifoS wf, fifoR wf